$\forall$$l$:IdLnk, ${\it dt}$:fpf(Id; ${\it tg}$.Type), ${\it knd}$:Knd, $T$:Type.
\\[0ex](($\uparrow$isrcv(${\it knd}$))
\\[0ex]$\Rightarrow$ ($\uparrow$eq\_lnk(lnk(${\it knd}$); $l$))
\\[0ex]$\Rightarrow$ ($\uparrow$fpf{-}dom(id{-}deq; tag(${\it knd}$); ${\it dt}$))
\\[0ex]$\Rightarrow$ ($T$ = fpf{-}ap(${\it dt}$; id{-}deq; tag(${\it knd}$))))
\\[0ex]$\Rightarrow$ fpf{-}compatible(Knd; $x$.Type; Kind{-}deq; lnk{-}decl($l$; ${\it dt}$); fpf{-}single(${\it knd}$; $T$))